M:MsgA, x:Id. x declared in M  Prop 

latex

Definitions	Id, t  T, x:A. B(x), x. t(x), Top, a:A fp B(a), IdDeq, x  dom(f), b, Prop, x declared in M, MsgA
Lemmas	msga wf, assert wf, fpf-dom wf, id-deq wf, fpf-trivial-subtype-top, Id wf